Inference at * 1 1 
Iof proof for Lemma fast-fib:



1. a : 
2. b : 
  {m:| 
  {k:.
  {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(0+k))}  

latex

 by (UseWitness a) 
CollapseTHEN (Auto) 

latex

C.

Definitions	, s = t, -n, n - m, , {x:A| B(x)} , , A, False, x:AB(x), Void, a < b, fib(n), n+m, P  Q, A  B, x:A. B(x), #$n, t  T
Lemmas	nat wf, fib wf, le wf